CHOICE-STRATEGY-IS: 
@(SUPPORT C2);

EDIT-STRATEGY-IS: 
α(C)>4∨∂(C)>2;


PARMODULATE =T
EQUAL-SYMBOL =NIL
PAR-DEPTH-BOUND =3
ELAPSED-TIME =583919

NIL 1 20
1 B(THEOREM4);3 22
3 A(0)⊃B(X)∨A(X);5 21
5 A(0)⊃B('(INDUCT3));7 20
7 A(0)⊃B('(INDUCT3))∨B(THEOREM4);9 22
9 A(0)⊃B('(INDUCT3))∨(B(X)∨A(X));11 12
11 A(0)⊃B('(INDUCT3))∨A('(INDUCT3));13 14
12 A('(INDUCT3))∧A(0)⊃B(X)∨A(X);INDUCT
13 A(0)⊃B(INDUCT3)∨A('(INDUCT3));15 16
14 B(X)⊃B('(X))∨A('(X));STEP
15 A(INDUCT3)∧A(0)⊃A('(INDUCT3));17 18
16 A(0)⊃B(INDUCT3)∨(B(X)∨(A(INDUCT3)∨A(X)));INDUCT
17 ¬(B('(INDUCT3))∧A(0));19 20
18 A(X)⊃B('(X))∨A('(X));STEP
19 B('(INDUCT3))∧A(0)⊃B(THEOREM4);21 22
20 ¬B(THEOREM4);THEOREM
21 B('(INDUCT3))∧A(0)⊃B(X)∨A(X);INDUCT
22 ¬A(THEOREM4);THEOREM